Inference at * 1 3 
Iof proof for Lemma last-not-before:



1. T : Type
2. L : T List
3. (null(L))
4. no_repeats(T;L)
5. x : T
6. last(L) before x  L
7. x, y:T. x before y  L  ((x = y))
8. (last(L) = x)
9. x before last(L)  L
  False 

latex

 by InteriorProof ((FLemma `l_before_transitivity` [6;9]) 
CollapseTHEN (MaAuto)) 

latex

C1: 

C1: 10. last(L) before last(L)  L
C1:   False
C.

Definitions	t  T, , last(L), null(as), s = t, L1  L2, x:A. B(x), x:A  B(x), x before y  l, no_repeats(T;l), x:A. B(x), A, b, P  Q, x:AB(x), Void, type List, False, Type
Lemmas	l before transitivity, assert wf